rank-1 typeとrank-2 typeの違い
from Rank N Polymorphism
rank-1 typeとrank-2 typeの違い
それぞれ
その関数を定義する時
その関数を呼び出す時
で見ていくと違いがわかりやすい
rank-1 typeな関数rank1について見る
定義する時
以下のような関数rank1を定義すると、型エラーになる
code:hs
rank1 :: forall a. (a -> Int) -> Int
rank1 f0 = f0 1,2,3 -- error
任意の型aに対して、「([a] -> Int) -> Int」という関数
関数のスコープに入った時点で、aは何らかの具体的な型に決定されている
だから、rank1の定義内、つまり=の右辺では、f0は多相関数ではない
何らかの具体的な型tに対して、[t] -> Intという型になっている
このtは、Intかもかしれないし、Charかもしれない
何かはわからないが、何か1つに決定されている
だから、定義内でf0 [1,2,3]という呼び出しはできない
なぜなら、f0 :: [Char] -> Intとなっている可能性がある
その場合、f0 [1,2,3]は明らかに間違っている
以下のような関数が定義できないのも全く同じ理由
code:hs
rank1' :: forall a. (a -> Int) -> Int
rank1' f0 = f0 1,2,3 + f0 'a','b','c' -- error
code:hs
rank1' :: (a -> Int) -> Int
rank1' f1 = f1 1,2,3 + f1 'a','b','c' -- error
呼び出す時
以下はいずれも型errorは発生しない
code:hs
ok = rank1 lengthInt
ok' = rank1 length
length' :: a -> Int
length' = length
lengthInt :: Int -> Int
lengthInt = length
length'、lengthIntは実装は全く同じで、型のみが異なる
なぜ型errorにならないか？
rank1の第1引数は、[t] -> Intという形なら何でもいい
ここでtは何らかの具体的な型
「任意の型」という意味ではないことに注意mrsekut.icon
多相化されているかどうかは問わない
具体的な型Intでも良いし、多相化されている∀ a. aでも良い
rank-2 typeな関数rank2について見る
定義する時
以下のような関数rank2の定義は、型errorにならない
code:hs
rank2 :: (forall a. a -> Int) -> Int
rank2 f1 = f1 1,2,3
「任意の型aに対して、([a] -> Int)」な関数を引数にとって、 Int型を返すという関数
rank1とは、forallのかかる位置が異なる
aのスコープは「...」の中だけ
rank2のbodyの中でもf1は多相化されている
f1は多相関数として、rank2の内部で扱うことができる
aは具体的な型ではなく、任意の型になる
逆に、具体的な型に決定されていてはいけない(後述)
全く同じ理由で、以下のような関数も定義できる
code:hs
rank2' :: (forall a. a -> Int) -> Int
rank2' f1 = f1 1,2,3 + f1 'a','b','c'
個々のf1でaのスコープが独立する
呼び出す時
rank2には、多相関数しか渡すことができない
code:ng.hs
ng = rank2 lengthInt -- ng
ok = rank2 length'
length' :: a -> Int
length' = length
lengthInt :: Int -> Int
lengthInt = length
length'、lengthIntは実装は全く同じで、型のみが異なる
lengthIntは[Int]に対してのみ適用できる関数
具体化されており、多相関数ではない
そのため、lengthIntは、rank2にわたすことはできない
これが渡せてしまうと、例えば以下のような不整合が起きる
code:hs
rank2' :: (forall a. a -> Int) -> Int
rank2' f1 = f1 1,2,3 + f1 'a','b','c'
という定義だった場合、2つめのf1の方で型が一致していない